$\forall$$T$:Type, $c$:$T$, $i$:Id. AtomFree(Type;$T$) $\Rightarrow$ $\vdash$${\it es}$.vartype($i$;"x") $\subseteq\rho$ $T$ \& $\forall$$e$@$i$. ("x" when $e$) $=$ $c$